i:Id, A:MsgA, M:System. (A ||+ M(i))  @i: A || M 

latex

Definitions	t  T, {T}, P  Q, x:A. B(x), SQType(T), Id, s = t, Prop, s ~ t, x:AB(x), x:AB(x), f(a), b, Type, A, b, , a = b, P & Q, P  Q, Unit, left+right, @i: A, A ||+ B, A || B, System, MsgA
Lemmas	ma-compat wf, msystem wf, msga wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, bnot wf, not wf, assert wf, ma-empty-compat-left, Id wf, Id sq